Inference at * 
Iof proof for Lemma sub functionality wrt le:


  i1, i2, j1, j2:. (i1  j1)  (i2  j2 )  ((i1 - i2)  (j1 - j2)) 

latex

 by (Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term) 

latex

 1: 

 1: 1. i1 : 
 1: 2. i2 : 
 1: 3. j1 : 
 1: 4. j2 : 
 1: 5. i1  j1
 1: 6. i2  j2 
 1:   (i1 - i2)  (j1 - j2)
 .

Definitions	t  T, P  Q, x:A. B(x),
Lemmas	le wf, ge wf